\begin{tabbing}
$\forall$\=${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} , $p$,\+
\\[0ex]$q$:(\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow$\{$e$:E$\mid$ loc($e$) = loc($e_{1}$) $\in$ Id\} $\rightarrow\mathbb{P}$).
\-\\[0ex]$e_{1}$ $\leq$loc $e_{2}$  $\Rightarrow$ $q$($e_{1}$,$e_{2}$) $\Rightarrow$ [$e_{1}$;$e_{2}$]$\sim$([$a$,$b$].$p$($a$,$b$))$\ast$[$a$,$b$].$q$($a$,$b$)
\end{tabbing}